x:Top, a:Atom1. x:Top>>a 

latex

Definitions	x:A. B(x), t  T, Top, A, P  Q, False, Prop
Lemmas	not wf, inheres wf, top wf, inherence-trivial